$\forall$${\it es}$:ES, ${\it ff}$:FIFO, ${\it f2f+}$:F2F+{-}decls.
\\[0ex](${\it ff}$.C $\subseteq$r Id) \& ($\forall$$i$, $j$:${\it ff}$.C. @$i$(awaiting ($i$,$j$):$\mathbb{B}$)) \& ($\forall$$i$, $j$:${\it ff}$.C. @$i$(owes\_ack ($i$,$j$):$\mathbb{B}$))
\\[0ex]\& ($\forall$$i$:${\it ff}$.C, $e$:E. (${\it ff}$.R($i$,$e$)) $\Rightarrow$ (loc($e$) = $i$ $\in$ Id))
\\[0ex]\& ($\forall$$e$:E. Dec(is\_req  ($e$)))
\\[0ex]\& ($\forall$$e$:E. Dec(is\_ack ($e$)))
\\[0ex]\& ($\forall$$i$:${\it ff}$.C, $e$:E. Dec(${\it ff}$.R($i$,$e$)))
\\[0ex]\& ($\forall$$i$, $j$:${\it ff}$.C, $e$:E. Dec(${\it ff}$.S($i$,$j$,$e$)))
\\[0ex]\& ($\forall$$i$, $j$:${\it ff}$.C, $e$:E. (${\it ff}$.S($i$,$j$,$e$)) $\Rightarrow$ (loc($e$) = $i$ $\in$ Id))
\\[0ex]\& ($\forall$$e$:E, ${\it sndr}$, ${\it rcvr}$:${\it ff}$.C. $\neg$([$e$: ${\it sndr}$ $--$is\_req  $\rightarrow$ ${\it rcvr}$] \& [$e$: ${\it rcvr}$ $--$is\_ack $\rightarrow$ ${\it sndr}$]))